YES 1.308 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule List
  ((isSuffixOf :: [Ratio Int ->  [Ratio Int ->  Bool) :: [Ratio Int ->  [Ratio Int ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] _ True
isPrefixOf [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule List
  ((isSuffixOf :: [Ratio Int ->  [Ratio Int ->  Bool) :: [Ratio Int ->  [Ratio Int ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule List
  (isSuffixOf :: [Ratio Int ->  [Ratio Int ->  Bool)

module List where
  import qualified Maybe
import qualified Prelude

  isPrefixOf :: Eq a => [a ->  [a ->  Bool
isPrefixOf [] vw True
isPrefixOf vx [] False
isPrefixOf (x : xs) (y : ysx == y && isPrefixOf xs ys

  isSuffixOf :: Eq a => [a ->  [a ->  Bool
isSuffixOf x y reverse x `isPrefixOf` reverse y


module Maybe where
  import qualified List
import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(ww16000), Succ(ww190000)) → new_primEqNat(ww16000, ww190000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_asAs(True, ww32, ww33, app(ty_Ratio, ba)) → new_esEs(ww32, ww33, ba)
new_esEs(:%(ww160, ww161), :%(ww1900, ww1901), bb) → new_asAs(new_esEs0(ww160, ww1900, bb), ww161, ww1901, bb)

The TRS R consists of the following rules:

new_primEqNat0(Zero, Succ(ww190000)) → False
new_primEqNat0(Succ(ww16000), Zero) → False
new_esEs2(Neg(Succ(ww1600)), Neg(Zero)) → False
new_esEs2(Neg(Zero), Neg(Succ(ww19000))) → False
new_esEs2(Pos(Zero), Pos(Zero)) → True
new_esEs2(Neg(Succ(ww1600)), Neg(Succ(ww19000))) → new_primEqNat0(ww1600, ww19000)
new_esEs2(Neg(Zero), Neg(Zero)) → True
new_esEs0(ww160, ww1900, ty_Integer) → new_esEs1(ww160, ww1900)
new_esEs1(ww16, ww190) → error([])
new_esEs2(Pos(Succ(ww1600)), Pos(Succ(ww19000))) → new_primEqNat0(ww1600, ww19000)
new_esEs0(ww160, ww1900, ty_Int) → new_esEs2(ww160, ww1900)
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(ww16000), Succ(ww190000)) → new_primEqNat0(ww16000, ww190000)
new_esEs2(Neg(Succ(ww1600)), Pos(ww1900)) → False
new_esEs2(Pos(Zero), Neg(Succ(ww19000))) → False
new_esEs2(Pos(Succ(ww1600)), Neg(ww1900)) → False
new_esEs2(Neg(Zero), Pos(Succ(ww19000))) → False
new_esEs2(Pos(Zero), Neg(Zero)) → True
new_esEs2(Neg(Zero), Pos(Zero)) → True
new_esEs2(Pos(Zero), Pos(Succ(ww19000))) → False
new_esEs2(Pos(Succ(ww1600)), Pos(Zero)) → False

The set Q consists of the following terms:

new_esEs2(Neg(Zero), Neg(Succ(x0)))
new_esEs1(x0, x1)
new_primEqNat0(Succ(x0), Zero)
new_esEs2(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs2(Pos(Zero), Neg(Zero))
new_esEs2(Neg(Zero), Pos(Zero))
new_primEqNat0(Zero, Zero)
new_esEs0(x0, x1, ty_Int)
new_esEs0(x0, x1, ty_Integer)
new_primEqNat0(Zero, Succ(x0))
new_esEs2(Neg(Succ(x0)), Neg(Zero))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs2(Pos(Succ(x0)), Pos(Zero))
new_esEs2(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs2(Pos(Zero), Pos(Zero))
new_esEs2(Neg(Zero), Neg(Zero))
new_esEs2(Neg(Succ(x0)), Pos(x1))
new_esEs2(Pos(Succ(x0)), Neg(x1))
new_esEs2(Pos(Zero), Neg(Succ(x0)))
new_esEs2(Neg(Zero), Pos(Succ(x0)))
new_esEs2(Pos(Zero), Pos(Succ(x0)))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_asAs0(True, :(ww250, ww251), :(ww260, ww261), ba) → new_asAs0(new_esEs3(ww250, ww260, ba), ww251, ww261, ba)

The TRS R consists of the following rules:

new_asAs1(True, ww32, ww33, app(app(app(ty_@3, bf), bg), bh)) → new_esEs8(ww32, ww33, bf, bg, bh)
new_asAs1(True, ww32, ww33, ty_Float) → new_esEs4(ww32, ww33)
new_esEs14(ww16, ww190, eg, eh) → error([])
new_esEs3(ww250, ww260, ty_Float) → new_esEs4(ww250, ww260)
new_esEs6(:%(ww160, ww161), :%(ww1900, ww1901), fa) → new_asAs1(new_esEs0(ww160, ww1900, fa), ww161, ww1901, fa)
new_esEs0(ww160, ww1900, ty_Integer) → new_esEs1(ww160, ww1900)
new_esEs7(ww16, ww190) → error([])
new_esEs3(ww250, ww260, app(ty_Ratio, db)) → new_esEs6(ww250, ww260, db)
new_asAs1(False, ww32, ww33, bc) → False
new_esEs5(ww16, ww190, bb) → error([])
new_esEs0(ww160, ww1900, ty_Int) → new_esEs2(ww160, ww1900)
new_primEqNat0(Zero, Zero) → True
new_esEs4(ww16, ww190) → error([])
new_esEs2(Pos(Zero), Neg(Zero)) → True
new_esEs2(Neg(Zero), Pos(Zero)) → True
new_esEs3(ww250, ww260, ty_Bool) → new_esEs9(ww250, ww260)
new_asAs1(True, ww32, ww33, app(ty_Ratio, bd)) → new_esEs6(ww32, ww33, bd)
new_esEs8(ww16, ww190, ed, ee, ef) → error([])
new_esEs3(ww250, ww260, ty_@0) → new_esEs12(ww250, ww260)
new_esEs13(ww16, ww190) → error([])
new_asAs1(True, ww32, ww33, ty_Int) → new_esEs2(ww32, ww33)
new_asAs1(True, ww32, ww33, app(app(ty_@2, ca), cb)) → new_esEs11(ww32, ww33, ca, cb)
new_esEs12(ww16, ww190) → error([])
new_asAs1(True, ww32, ww33, ty_Ordering) → new_esEs13(ww32, ww33)
new_primEqNat0(Zero, Succ(ww190000)) → False
new_primEqNat0(Succ(ww16000), Zero) → False
new_asAs1(True, ww32, ww33, ty_@0) → new_esEs12(ww32, ww33)
new_asAs1(True, ww32, ww33, ty_Bool) → new_esEs9(ww32, ww33)
new_esEs2(Neg(Zero), Neg(Zero)) → True
new_esEs3(ww250, ww260, ty_Double) → new_esEs7(ww250, ww260)
new_esEs1(ww16, ww190) → error([])
new_asAs1(True, ww32, ww33, ty_Double) → new_esEs7(ww32, ww33)
new_esEs10(ww16, ww190) → error([])
new_esEs3(ww250, ww260, app(ty_Maybe, ec)) → new_esEs15(ww250, ww260, ec)
new_esEs3(ww250, ww260, app(app(ty_Either, ea), eb)) → new_esEs14(ww250, ww260, ea, eb)
new_esEs3(ww250, ww260, ty_Integer) → new_esEs1(ww250, ww260)
new_asAs1(True, ww32, ww33, app(ty_Maybe, ce)) → new_esEs15(ww32, ww33, ce)
new_esEs3(ww250, ww260, app(app(ty_@2, dg), dh)) → new_esEs11(ww250, ww260, dg, dh)
new_esEs3(ww250, ww260, ty_Int) → new_esEs2(ww250, ww260)
new_esEs2(Neg(Succ(ww1600)), Neg(Zero)) → False
new_esEs2(Neg(Zero), Neg(Succ(ww19000))) → False
new_esEs11(ww16, ww190, cf, cg) → error([])
new_esEs2(Neg(Succ(ww1600)), Neg(Succ(ww19000))) → new_primEqNat0(ww1600, ww19000)
new_primEqNat0(Succ(ww16000), Succ(ww190000)) → new_primEqNat0(ww16000, ww190000)
new_esEs3(ww250, ww260, app(app(app(ty_@3, dd), de), df)) → new_esEs8(ww250, ww260, dd, de, df)
new_esEs2(Pos(Zero), Neg(Succ(ww19000))) → False
new_esEs2(Neg(Zero), Pos(Succ(ww19000))) → False
new_esEs3(ww250, ww260, ty_Char) → new_esEs10(ww250, ww260)
new_asAs1(True, ww32, ww33, app(app(ty_Either, cc), cd)) → new_esEs14(ww32, ww33, cc, cd)
new_esEs2(Pos(Zero), Pos(Succ(ww19000))) → False
new_esEs2(Pos(Succ(ww1600)), Pos(Zero)) → False
new_asAs1(True, ww32, ww33, ty_Char) → new_esEs10(ww32, ww33)
new_esEs2(Pos(Zero), Pos(Zero)) → True
new_asAs1(True, ww32, ww33, app(ty_[], be)) → new_esEs5(ww32, ww33, be)
new_esEs3(ww250, ww260, ty_Ordering) → new_esEs13(ww250, ww260)
new_esEs9(ww16, ww190) → error([])
new_esEs2(Pos(Succ(ww1600)), Pos(Succ(ww19000))) → new_primEqNat0(ww1600, ww19000)
new_esEs2(Pos(Succ(ww1600)), Neg(ww1900)) → False
new_esEs2(Neg(Succ(ww1600)), Pos(ww1900)) → False
new_asAs1(True, ww32, ww33, ty_Integer) → new_esEs1(ww32, ww33)
new_esEs15(ww16, ww190, da) → error([])
new_esEs3(ww250, ww260, app(ty_[], dc)) → new_esEs5(ww250, ww260, dc)

The set Q consists of the following terms:

new_esEs15(x0, x1, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs0(x0, x1, ty_Integer)
new_esEs3(x0, x1, ty_Bool)
new_asAs1(True, x0, x1, app(ty_Ratio, x2))
new_esEs14(x0, x1, x2, x3)
new_esEs2(Neg(Succ(x0)), Neg(Zero))
new_esEs3(x0, x1, ty_Integer)
new_esEs3(x0, x1, ty_Float)
new_esEs9(x0, x1)
new_asAs1(True, x0, x1, ty_Double)
new_asAs1(True, x0, x1, ty_Int)
new_esEs8(x0, x1, x2, x3, x4)
new_esEs2(Neg(Zero), Neg(Succ(x0)))
new_esEs12(x0, x1)
new_esEs3(x0, x1, app(ty_[], x2))
new_esEs2(Pos(Zero), Neg(Zero))
new_esEs2(Neg(Zero), Pos(Zero))
new_esEs5(x0, x1, x2)
new_esEs4(x0, x1)
new_asAs1(True, x0, x1, ty_@0)
new_asAs1(True, x0, x1, app(ty_[], x2))
new_asAs1(True, x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs2(Neg(Zero), Pos(Succ(x0)))
new_esEs2(Pos(Zero), Neg(Succ(x0)))
new_asAs1(True, x0, x1, ty_Char)
new_asAs1(True, x0, x1, ty_Integer)
new_esEs6(:%(x0, x1), :%(x2, x3), x4)
new_asAs1(True, x0, x1, app(app(ty_@2, x2), x3))
new_esEs3(x0, x1, app(ty_Ratio, x2))
new_esEs11(x0, x1, x2, x3)
new_esEs3(x0, x1, app(app(ty_@2, x2), x3))
new_asAs1(True, x0, x1, ty_Float)
new_esEs2(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs3(x0, x1, ty_Ordering)
new_esEs0(x0, x1, ty_Int)
new_primEqNat0(Zero, Succ(x0))
new_asAs1(True, x0, x1, app(app(ty_Either, x2), x3))
new_esEs3(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs2(Pos(Succ(x0)), Pos(Zero))
new_esEs2(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs2(Pos(Zero), Pos(Zero))
new_asAs1(False, x0, x1, x2)
new_asAs1(True, x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1)
new_esEs3(x0, x1, ty_Double)
new_esEs3(x0, x1, app(ty_Maybe, x2))
new_esEs1(x0, x1)
new_asAs1(True, x0, x1, ty_Ordering)
new_esEs3(x0, x1, ty_@0)
new_esEs3(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs13(x0, x1)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs2(Neg(Zero), Neg(Zero))
new_esEs10(x0, x1)
new_esEs2(Pos(Succ(x0)), Neg(x1))
new_esEs2(Neg(Succ(x0)), Pos(x1))
new_esEs3(x0, x1, ty_Char)
new_asAs1(True, x0, x1, ty_Bool)
new_esEs2(Pos(Zero), Pos(Succ(x0)))
new_esEs3(x0, x1, ty_Int)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf(ww16, ww15, ww19, :(ww1810, ww1811), ba) → new_isPrefixOf(ww16, ww15, new_flip(ww19, ww1810, ba), ww1811, ba)

The TRS R consists of the following rules:

new_flip(ww15, ww16, ba) → :(ww16, ww15)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_isPrefixOf0(ww15, ww16, :(ww170, ww171), ww18, ba) → new_isPrefixOf0(new_flip(ww15, ww16, ba), ww170, ww171, ww18, ba)

The TRS R consists of the following rules:

new_flip(ww15, ww16, ba) → :(ww16, ww15)

The set Q consists of the following terms:

new_flip(x0, x1, x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: